$\forall$$T$:Type. finite($T$) $\in$ Prop